(0) Obligation:
The Runtime Complexity (innermost) of the given
CpxTRS could be proven to be
BOUNDS(1, n^1).
The TRS R consists of the following rules:
h(X, Z) → f(X, s(X), Z)
f(X, Y, g(X, Y)) → h(0, g(X, Y))
g(0, Y) → 0
g(X, s(Y)) → g(X, Y)
Rewrite Strategy: INNERMOST
(1) NestedDefinedSymbolProof (BOTH BOUNDS(ID, ID) transformation)
The TRS does not nest defined symbols.
Hence, the left-hand sides of the following rules are not basic-reachable and can be removed:
f(X, Y, g(X, Y)) → h(0, g(X, Y))
(2) Obligation:
The Runtime Complexity (innermost) of the given
CpxTRS could be proven to be
BOUNDS(1, n^1).
The TRS R consists of the following rules:
h(X, Z) → f(X, s(X), Z)
g(X, s(Y)) → g(X, Y)
g(0, Y) → 0
Rewrite Strategy: INNERMOST
(3) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)
Converted Cpx (relative) TRS to CDT
(4) Obligation:
Complexity Dependency Tuples Problem
Rules:
h(z0, z1) → f(z0, s(z0), z1)
g(z0, s(z1)) → g(z0, z1)
g(0, z0) → 0
Tuples:
H(z0, z1) → c
G(z0, s(z1)) → c1(G(z0, z1))
G(0, z0) → c2
S tuples:
H(z0, z1) → c
G(z0, s(z1)) → c1(G(z0, z1))
G(0, z0) → c2
K tuples:none
Defined Rule Symbols:
h, g
Defined Pair Symbols:
H, G
Compound Symbols:
c, c1, c2
(5) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)
Removed 2 trailing nodes:
H(z0, z1) → c
G(0, z0) → c2
(6) Obligation:
Complexity Dependency Tuples Problem
Rules:
h(z0, z1) → f(z0, s(z0), z1)
g(z0, s(z1)) → g(z0, z1)
g(0, z0) → 0
Tuples:
G(z0, s(z1)) → c1(G(z0, z1))
S tuples:
G(z0, s(z1)) → c1(G(z0, z1))
K tuples:none
Defined Rule Symbols:
h, g
Defined Pair Symbols:
G
Compound Symbols:
c1
(7) CdtUsableRulesProof (EQUIVALENT transformation)
The following rules are not usable and were removed:
h(z0, z1) → f(z0, s(z0), z1)
g(z0, s(z1)) → g(z0, z1)
g(0, z0) → 0
(8) Obligation:
Complexity Dependency Tuples Problem
Rules:none
Tuples:
G(z0, s(z1)) → c1(G(z0, z1))
S tuples:
G(z0, s(z1)) → c1(G(z0, z1))
K tuples:none
Defined Rule Symbols:none
Defined Pair Symbols:
G
Compound Symbols:
c1
(9) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)) transformation)
Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.
G(z0, s(z1)) → c1(G(z0, z1))
We considered the (Usable) Rules:none
And the Tuples:
G(z0, s(z1)) → c1(G(z0, z1))
The order we found is given by the following interpretation:
Polynomial interpretation :
POL(G(x1, x2)) = x2
POL(c1(x1)) = x1
POL(s(x1)) = [1] + x1
(10) Obligation:
Complexity Dependency Tuples Problem
Rules:none
Tuples:
G(z0, s(z1)) → c1(G(z0, z1))
S tuples:none
K tuples:
G(z0, s(z1)) → c1(G(z0, z1))
Defined Rule Symbols:none
Defined Pair Symbols:
G
Compound Symbols:
c1
(11) SIsEmptyProof (BOTH BOUNDS(ID, ID) transformation)
The set S is empty
(12) BOUNDS(1, 1)